#ifndef TRANSLATOR_H
#define TRANSLATOR_H
#include "core/Solver.h"
#include "cdnf.h"
#include "valuation.h"
#include <string>
using namespace cdnf;

void loadVars(std::string filename,int numberOfVar);
Minisat::Lit convert2CNF(CDNF& cdnf,Minisat::Solver* solver,int offset,int* vars);
Minisat::Lit convert2CNF(CDNF& cdnf,Minisat::Solver* solver,bool flag,int* vars);
Minisat::Lit convert2CNF(CDNF& cdnf,Minisat::Solver* solver,bool flag,int offset,int* vars);
Minisat::Lit convert2CNF(DNF& dnf,Minisat::Solver* solver,bool flag,int offset,int* vars);
void setDecisionVars(Minisat::Solver* solver,int* vars,int end);
void setDecisionVars(Minisat::Solver* solver,int* vars,int start,int end);
void getInput(Minisat::Solver* solver,int input,int latch,int* vars,bool* valuation);
void getPre(Minisat::Solver* solver,int numberOfVar,int* vars,Valuation& valuation);
void getPost(Minisat::Solver* solver,int numberOfVar,int offset,int* vars,Valuation& valuation);
void logMessage(std::string message);
std::string printCDNF(CDNF& cdnf);
std::string printDNF(DNF& dnf);

#endif
